Erasure-Branch-On-Erased.agda:8,1-9,8
Cannot branch on erased argument of datatype Bool
when checking the definition of T
